finite{-}type($T$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$$n$:$\mathbb{N}$. $\exists$$f$:int\_seg(0; $n$)$\rightarrow$$T$. surject(int\_seg(0; $n$); $T$; $f$)